#ifndef _AST_VISITOR_HPP
#define	_AST_VISITOR_HPP

#include <cstdlib>
#include <cstdio>
#include <iostream>
#include <fstream>
#include <string>
#include <vector>
#include <stack>
#include <list>
#include <map>
#include <set>
#include <cassert>
#include <boost/format.hpp>
#include "ast.hpp"
#include "cfg.hpp"
#include "dot.hpp"
#include "lex_cast.h"
#include "util.hpp"
#include "Interval.hpp"
#include "monotone_framework.hpp"
#include "hashing.hpp"
#include "global_vars.hpp"
#include "set_operations.hpp"

#define VISIT(x)	{ if(x) {(x)->acceptVisit(this);} }
//#define NO_PREDS

using namespace std;

class box;
class CFGedge;
class dot;

class ASTnode;
class arith;
class lvalue;
class constant;
class variable;
class array_element;
class anegation;
class aplus;
class aminus;
class amultiply;
class adivide;
class binary_operator;

class b_true;
class b_false;
class b_not;
class b_and;
class b_or;
class b_gt;
class b_ge;
class b_lt;
class b_le;
class b_eq;
class b_neq;
class b_relational;

class s_skip;
class s_read;
class s_write;
class s_if;
class s_while;
class sequence;
class assignment;
class program;

class CFGvertex;
class diamond;
class atomic_statement;


class ASTvisitor {
public:
	virtual void StartVisit(ASTnode *n) = 0;
	virtual void visit(constant *n);
	virtual void visit(variable *n);
	virtual void visit(array_element *n);
	virtual void visit(anegation *n);
	virtual void visit(aplus *n);
	virtual void visit(aminus *n);
	virtual void visit(amultiply *n);
	virtual void visit(adivide *n);

	virtual void visit(b_true *n);
	virtual void visit(b_false *n);
	virtual void visit(b_not *n);
	virtual void visit(b_and *n);
	virtual void visit(b_or *n);
	virtual void visit(b_gt *n);
	virtual void visit(b_ge *n);
	virtual void visit(b_lt *n);
	virtual void visit(b_le *n);
	virtual void visit(b_eq *n);
	virtual void visit(b_neq *n);

	virtual void visit(s_skip *n);	
	virtual void visit(s_read *n);	
	virtual void visit(s_write *n);	
	virtual void visit(s_if *n);	
	virtual void visit(s_while *n);	
	virtual void visit(sequence *n);	
	virtual void visit(assignment *n);
	virtual void visit(program *n);
};


class ASTvisitorDOT : public ASTvisitor {
public:
	ASTvisitorDOT();
	~ASTvisitorDOT();
	void writeDOTfile(const char *fPath);

	void StartVisit(ASTnode *n);
	void visit(constant *n);
	void visit(variable *n);
	void visit(array_element *n);
	void visit(anegation *n);
	void visit(aplus *n);
	void visit(aminus *n);
	void visit(amultiply *n);
	void visit(adivide *n);

	void visit(b_true *n);
	void visit(b_false *n);
	void visit(b_not *n);
	void visit(b_and *n);
	void visit(b_or *n);
	void visit(b_gt *n);
	void visit(b_ge *n);
	void visit(b_lt *n);
	void visit(b_le *n);
	void visit(b_eq *n);
	void visit(b_neq *n);
	
	void visit(s_skip *n);	
	void visit(s_read *n);	
	void visit(s_write *n);	
	void visit(s_if *n);	
	void visit(s_while *n);	
	void visit(sequence *n);	
	void visit(assignment *n);
	void visit(program *n);

private:
	inline void handle_children(b_relational *n);
	inline void handle_children(binary_operator *n);
	
	dot	*graf;	// En visitorDOT skriver til en graf
};

class ASTvisitorString : public ASTvisitor {
public:
	string convert(ASTnode *n);
	void StartVisit(ASTnode *n);
	void visit(constant *n);
	void visit(variable *n);
	void visit(array_element *n);
	void visit(anegation *n);
	void visit(aplus *n);
	void visit(aminus *n);
	void visit(amultiply *n);
	void visit(adivide *n);

	void visit(b_true *n);
	void visit(b_false *n);
	void visit(b_not *n);
	void visit(b_and *n);
	void visit(b_or *n);
	void visit(b_gt *n);
	void visit(b_ge *n);
	void visit(b_lt *n);
	void visit(b_le *n);
	void visit(b_eq *n);
	void visit(b_neq *n);
	
	void visit(s_skip *n);	
	void visit(s_read *n);
	void visit(s_write *n);	
	void visit(s_if *n);	
	void visit(s_while *n);	
	void visit(sequence *n);	
	void visit(assignment *n);
	void visit(program *n);
private:
	void remove_outer_parens(string& arg);
	string result;
};

class ASTvisitorFV : public ASTvisitor {
public:
	void StartVisit(ASTnode *n);
	set<lvalue*> getFV() const;
	void visit(variable *n);
	void visit(array_element *n);

private:
	set<lvalue*> fv;
};

class ASTvisitorUses : public ASTvisitor {
public:
	set<string> convert(ASTnode *n);
	void StartVisit(ASTnode *n);
	void visit(variable *n);
	void visit(array_element *n);
	void visit(assignment *n);
	void visit(s_write *n);
	void visit(s_read *n);
private:
	set<string> uses;
};

class ASTvisitorDefs : public ASTvisitor {
public:
	void StartVisit(ASTnode *n);
	set<string> getDefs() const;
	void visit(variable *n);
	void visit(array_element *n);
	void visit(assignment *n);
	void visit(s_write *n);
	void visit(s_read *n);
private:
	set<string> defs;
};


class ASTvisitorCFG : public ASTvisitor {
public:
	CFGvertex* convert(ASTnode* n);
	void StartVisit(ASTnode *n);
	
	void visit(s_skip *n);
	void visit(s_read *n);	
	void visit(s_write *n);	
	void visit(assignment *n);
	void visit(s_if *n);	
	void visit(s_while *n);	
	void visit(sequence *n);
	void visit(program *n);

private:
	struct head_tail {
		CFGvertex*		head;
		set<CFGedge*>	tail;
		void append(const head_tail& addenum);
	};

	head_tail visit_getReturn(ASTnode *n);
	void Return(const head_tail& arg);
	void handle_atomic(atomic_statement *n);

	stack<head_tail> args;
};


/**
 * Detects the sign of given expression
 */
class ASTvisitorAs : public ASTvisitor {
public:

typedef string sign;	// restricted to -1,0,+1
typedef set<sign> signs;
typedef map<string/*var*/, signs> DS;
	
	ASTvisitorAs(DS& _sigma);
	Interval get_interval(ASTnode *n);	
	void StartVisit(ASTnode *n);
	void visit(constant *n);
	void visit(variable *n);
	void visit(array_element *n);
	void visit(aplus *n);
	void visit(aminus *n);
	void visit(amultiply *n);
	void visit(adivide *n);
	void visit(anegation *n);
private:
	Interval visit_getReturn(ASTnode *n);
	void Return(Interval ret_val);
	Interval lookup_in_sigma(const string& name);	
	stack<Interval> args;
	DS& sigma;
};

/**
 * Detects the interval of given expression
 */
class ASTvisitorAi : public ASTvisitor {
public:
	ASTvisitorAi(IV& _sigma);
	Interval get_interval(ASTnode *n);	
	IV get_new_sigma(bexp *n);
	void StartVisit(ASTnode *n);
	void visit(b_true *n);
	void visit(b_false *n);
	void visit(b_and *n);
	void visit(b_or *n);
	void visit(b_not *n);
	void visit(b_lt *n);
	void visit(b_gt *n);	
	void visit(b_ge *n);	
	void visit(b_le *n);	
	void visit(b_eq *n);	
	void visit(b_neq *n);	
	void visit(constant *n);
	void visit(variable *n);
	void visit(array_element *n);
	void visit(aplus *n);
	void visit(aminus *n);
	void visit(amultiply *n);
	void visit(adivide *n);
	void visit(anegation *n);
private:
	Interval visit_getReturn(ASTnode *n);
	void Return(Interval ret_val);
	stack<Interval> args;

	IV visit_getReturnIV(bexp *n);
	void ReturnIV(IV ret_val);
	stack<IV> argsIV;

	IV awesome(Interval i1_better, Interval i2_better, arith* arg1, arith* arg2);	
	Interval lookup_in_sigma(const string& name);	
	IV& sigma;
};


class ASTvisitorHash : public ASTvisitor {
public:
	hash_t convert(ASTnode *n);
	void StartVisit(ASTnode *n);
	void visit(constant *n);
	void visit(variable *n);
	void visit(array_element *n);
	void visit(aplus *n);
	void visit(aminus *n);
	void visit(amultiply *n);
	void visit(adivide *n);
	void visit(anegation *n);
	hash_t visit_getReturn(ASTnode *n);
private:
	void Return(hash_t ret_val);
	stack<hash_t> args;
};

class ASTvisitorGetArrays : public ASTvisitor {
public:
	set<array_element*> convert(ASTnode *n);
	void StartVisit(ASTnode *n);
	void visit(array_element *n);
private:
	set<array_element*> arrays;
};

Interval prune(const Interval& arg);	
void prune_test();
bool is_algebraically_equivalent(ASTnode *arg1, ASTnode *arg2);
IV project(arith *root, iint target_value, IV& orig_sigma);
void project_test();


#endif	/* _AST_VISITOR_HPP */
